@Article{hl07mechanizing,
  author = 	 {Robert Harper and Daniel R. Licata},
  title = 	 {Mechanizing Metatheory in a Logical Framework},
  journal = 	 {Journal of Functional Programming},
  year = 	 {2007},
  note = 	 {To appear. Available from \url{http://www.cs.cmu.edu/~drl/}},
}

@Book{L:BC04,
  author       = "Bertot, Yves and Cast\'eran, Pierre",
  title        = "Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions",
  series       = "Texts in Theoretical Computer Science",
  year         = "2004",
  publisher    = "Springer Verlag",
  url          = "http://www.labri.fr/publications/l3a/2004/BC04"
}

@Misc{girard:thesis,
  author = 	 {J.Y. Girard},
  title = 	 {Interpretation fonctionelle et elimination des coupures
                  de l'arithmetique d'ordre superieur},
  howpublished = {These d'Etat, Paris VII},
  year =	 1972
}

@TechReport{emir07:oopatmatch,
   abstract    = {Data in object-oriented programming is organized in a
                 hierarchy of classes. The problem of *object-oriented
                 pattern matching* is how to explore this hierarchy from
                 the outside. This usually involves classifying objects by
                 their run-time type, accessing their members, or
                 determining some other characteristic of a group of
                 objects. In this paper we compare six different pattern
                 matching techniques: object-oriented decomposition,
                 visitors, type-tests/type-casts, typecase, case classes,
                 and extractors. The techniques are compared on nine
                 criteria related to conciseness, maintainability and
                 performance. The paper introduces case classes and
                 extractors as two new pattern-matching methods and shows
                 that their combination works well for all of the
                 established criteria.},
   author      = {Emir, Burak and Odersky, Martin and Williams, John},
   details     = {http://infoscience.epfl.ch/search.py?recid=98468},
   documenturl = {http://infoscience.epfl.ch/getfile.py?recid=98468&mode=best},
   keywords    = {object-oriented programming; pattern matching; language
                 design; type systems; generalized algebraic data types},
   title       = {Matching {O}bjects with {P}atterns},
   unit        = {LAMP},
   note        = {To appear in the proceedings of ECOOP 2007.},
   year        = 2006
}

@TechReport{LAMP-REPORT-2006-001,
   abstract    = {Scala fuses object-oriented and functional programming
                 in a statically typed programming language. It is aimed
                 at the construction of components and component systems.
                 This paper gives an overview of the Scala language for
                 readers who are familar with programming methods and
                 programming language design.},
   author      = {Odersky, Martin and Altherr, Philippe and Cremet,
                 Vincent and Dragos, Iulian and Dubochet, Gilles and Emir,
                 Burak and McDirmid, Sean and Micheloud, St\'ephane and
                 Mihaylov, Nikolay and Schinz, Michel and Spoon, Lex and
                 Stenman, Erik and Zenger, Matthias},
   details     = {http://infoscience.epfl.ch/search.py?recid=85634},
   documenturl = {http://infoscience.epfl.ch/getfile.py?recid=85634&mode=best},
   keywords    = {components; programming language design; type systems;
                 web services; functional programming; object-oriented
                 programming; XML processing},
   title       = {An {O}verview of the {S}cala {P}rogramming {L}anguage (2. Edition)},
   unit        = {LAMP},
   year        = 2006
}

@TechReport{Henglein:SubtypingProperties:96,
  AUTHOR      = {Henglein, Fritz},
  YEAR        = {1996},
  TITLE       = {Syntactic Properties of Polymorphic Subtyping},
  INSTITUTION = {DIKU, University of Copenhagen},
  address     = {Universitetsparken 1, DK-2100 Copenhagen, Denmark},
  type        = {TOPPS Technical Report (D-report series)},
  number      = {D-293},
  month       = {May},
  keywords    = {Polymorphism, subtyping, type inference, syntactic
properties, principal type, Algorithm W, simplifications, qualified
type schemes, instance relation},
  summary     = {In this paper we study polymorphic subtyping, where the subtyping
theory is \emph{not} required to be structural.  We observe that type
schemes with subtyping qualifications are strictly necessary in order
to obtain principal typing.  We identify a new instance relation on
typing judgements, the \emph{halbstark} relation.  It is a hybrid,
lying in strength between Mitchell's original instance relation and
Fuh and Mishra's lazy instance relation.  We present a sound and
complete type inference algorithm in the style of Milner's Algorithm
W.  The significance of the halbstark relation emerges from the fact that
the algorithm is \emph{generic} in that it admits replacing 
typing judgements by \emph{any} halbstark-equivalent judgements at any
point.  This provides a generalized correctness argument for Algorithm W
independent of any particular constraint simplification strategy
chosen.  
Finally, we show that polymorphic typing judgements are
preserved under let-unfolding, let-folding, and
$\eta$-reduction, but not in general under $\beta$-reduction.  
The latter holds, though, if the subtyping discipline has the
\emph{decomposition} property, which says that two function types are
in a subtype relation only if their domain and range types are
in the appropriate contra-/covariant subtype relation.
},
  supersedes  = {},
  SEMNO       = {D-293},
  PUF         = {Tekniske rapport},
  ID          = {Tek}
}

@misc{Sheard:playing,
  author = "Tim Sheard",
  title = "Playing with Type Systems: Automated assistance in the design of
    programming langauges",
  note = {\url{http://web.cecs.pdx.edu/~sheard/papers/PlayingWithTypes2.ps}},
  year = 2006,
}

@inproceedings{citeulike:975433,
	author = {Tim Sheard},
	booktitle = {PLPV},
	keywords = {dependent-types provers},
	priority = {0},
	title = {Type-level Computation Using Narrowing in {$\Omega$}mega.},
	url = {http://web.cecs.pdx.edu/~sheard/papers/sheardPLPV.ps},
	year = {2006}
}

@misc{ott,
  author = "Peter Sewell and Francesco Zappa Nardelli and Scott Owens and Gilles Peskine and Thomas Ridge and Susmit Sarkar and Rok Strni\u{s}a",
  title = "Ott: Effective Tool Support for the Working Semanticist",
  note = {Draft from \url{http://www.cl.cam.ac.uk/~pes20/ott/paper.pdf}},
  year = 2007,
}

@INPROCEEDINGS{moors06:oodgp,
	AUTHOR = {Adriaan Moors and Frank Piessens and Wouter Joosen},
	TITLE = {An {O}bject-{O}riented {A}pproach to {D}atatype-{G}eneric {P}rogramming},
	YEAR = {2006},
	BOOKTITLE = {Proceedings of the Workshop on Generic Programming}	
}

@INPROCEEDINGS{gibbons06:hodgp,
	AUTHOR = {Jeremy Gibbons},
	TITLE = {Design {P}atterns as {H}igher-{O}rder {D}atatype-{G}eneric {P}rograms},
	YEAR = {2006},
	BOOKTITLE = {Proceedings of the Workshop on Generic Programming}	
}


@INPROCEEDINGS{ barnett-spec,
  author = "Mike Barnett and K. Rustan M. Leino and Wolfram Schulte",
  title = "The {S}pec# {P}rogramming {S}ystem: {A}n {O}verview",
  year = {2004},
  booktitle = {Prooceedings},
  url = "citeseer.ist.psu.edu/649115.html" }


@inproceedings{Barnett2005:specsharp,
  title = {The Spec# Programming System: An Overview},
  author = {Mike Barnett and K. Rustan M. Leino and Wolfram Schulte},
  booktitle = {Construction and Analysis of Safe, Secure, and Interoperable Smart Devices},
  publisher = {Springer Berlin / Heidelberg},
  issn = {0302-9743 (Print) 1611-3349 (Online)},
  url = {http://springerlink.com/content/0m789xre652nuv06/},
  abstract = {The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. This paper describes the goals and architecture of the Spec# programming system, consisting of the object-oriented Spec# programming language, the Spec# compiler, and the Boogie static program verifier. The language includes constructs for writing specifications that capture programmer intentions about how methods and data are to be used, the compiler emits run-time checks to enforce these specifications, and the verifier can check the consistency between a program and its specifications.},
  pages = {49--69},
  doi = {10.1007/b105030},
  year = {2005},
  month = {January},
}


@misc{kidd07:setmonad,
  author = "Eric Kidd",
  title = "How to make Data.Set a monad",
  year = 2007,
  note = {Blog post at \url{http://www.randomhacks.net/articles/2007/03/15/data-set-monad-haskell-macros}}
}

@misc{volder94:setmonad,
  author = "Kris De Volder",
  title = {constructor classes \& "set" monad?},
  year = 1994,
  note = {Messages on comp.lang.functional  \url{http://groups.google.com/group/comp.lang.functional/browse_thread/thread/5db5c013d529b653/e10290b2511c65f0}}
}
